Trong ngành khoa học máy tính, các phương pháp hình thức là các kỹ thuật toán học cho việc đặc tả, phát triển và kiểm định các hệ thống phần mềm và phần cứng. Cách tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, khi an toàn hay an ninh có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.